Inference at * 
Iof proof for Lemma test-rewrite-dcdr:


  P:, d:Dec(P). ([d])  (([d])) 

latex

 by ( RW assert_pushdownC 0) 
CollapseTHEN (MaAuto) 

latex

C.

Definitions	P  Q, P & Q, x:A  B(x), x. t(x), P  Q, P  Q, b, [d], , x.A(x), x:A. B(x), P  Q, left + right, A, x:AB(x), Dec(P), , Type, t  T
Lemmas	all functionality wrt iff, or functionality wrt iff, not functionality wrt iff, dcdr-to-bool-equivalence, decidable wf, dcdr-to-bool wf, assert wf, not wf